$\forall$${\it loc}$:Id, ${\it ds}$:fpf(Id; $x$.Type), $a$:Id, $p$:finite{-}prob{-}space, $P$:(decl{-}state(${\it ds}$)$\rightarrow\mathbb{B}$).
\\[0ex]Rpre(${\it loc}$; ${\it ds}$; $a$; $p$; $P$) $\in$ es\_realizer\{i:l\}